『Homotopy Type Theory Univalent Foundations of Mathematics』 目次

Contents

Introduction 1

I Foundations 15

1 Type theory 17

1.1 Type theory versus set theory . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 17

1.2 Function types . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 21

1.3 Universes and families . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 24

1.4 Dependent function types (Π-types) . . . . . . . . . . . . . . . . . . . . . . . . . . . 25

1.5 Product types . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 26

1.6 Dependent pair types (Σ-types) . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30

1.7 Coproduct types . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33

1.8 The type of booleans . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35

1.9 The natural numbers . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36

1.10 Pattern matching and recursion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40

1.11 Propositions as types . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41

1.12 Identity types . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47

Notes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54

Exercises . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 56

2 Homotopy type theory 59

2.1 Types are higher groupoids . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 62

2.2 Functions are functors . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 71

2.3 Type families are fibrations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 72

2.4 Homotopies and equivalences . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 76

2.5 The higher groupoid structure of type formers . . . . . . . . . . . . . . . . . . . . . 79

2.6 Cartesian product types . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 81

2.7 Σ-types . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 83

2.8 The unit type . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 86

2.9 Π-types and the function extensionality axiom . . . . . . . . . . . . . . . . . . . . . 86

2.10 Universes and the univalence axiom . . . . . . . . . . . . . . . . . . . . . . . . . . . 89

2.11 Identity type . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 91

2.12 Coproducts . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 93

2.13 Natural numbers . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 95

2.14 Example: equality of structures . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 97

2.15 Universal properties . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 100

Notes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 102

Exercises . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 104

3 Sets and logic 107

3.1 Sets and n-types . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 107

3.2 Propositions as types? . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 109

3.3 Mere propositions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 111

3.4 Classical vs. intuitionistic logic . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 113

3.5 Subsets and propositional resizing . . . . . . . . . . . . . . . . . . . . . . . . . . . . 114

3.6 The logic of mere propositions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 116

3.7 Propositional truncation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 117

3.8 The axiom of choice . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 118

3.9 The principle of unique choice . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 120

3.10 When are propositions truncated? . . . . . . . . . . . . . . . . . . . . . . . . . . . . 121

3.11 Contractibility . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 123

Notes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 126

Exercises . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 127

4 Equivalences 129

4.1 Quasi-inverses . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 130

4.2 Half adjoint equivalences . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 132

4.3 Bi-invertible maps . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 136

4.4 Contractible fibers . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 136

4.5 On the definition of equivalences . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 138

4.6 Surjections and embeddings . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 138

4.7 Closure properties of equivalences . . . . . . . . . . . . . . . . . . . . . . . . . . . . 139

4.8 The object classifier . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 142

4.9 Univalence implies function extensionality . . . . . . . . . . . . . . . . . . . . . . . 144

Notes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 146

Exercises . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 146

5 Induction 149

5.1 Introduction to inductive types . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 149

5.2 Uniqueness of inductive types . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 152

5.3 W-types . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 154

5.4 Inductive types are initial algebras . . . . . . . . . . . . . . . . . . . . . . . . . . . . 157

5.5 Homotopy-inductive types . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 160

5.6 The general syntax of inductive definitions . . . . . . . . . . . . . . . . . . . . . . . 164

5.7 Generalizations of inductive types . . . . . . . . . . . . . . . . . . . . . . . . . . . . 168

5.8 Identity types and identity systems . . . . . . . . . . . . . . . . . . . . . . . . . . . . 170

Notes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 174

Exercises . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 175

6 Higher inductive types 179

6.1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 179

6.2 Induction principles and dependent paths . . . . . . . . . . . . . . . . . . . . . . . . 181

6.3 The interval . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 186

6.4 Circles and spheres . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 187

6.5 Suspensions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 189

6.6 Cell complexes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 192

6.7 Hubs and spokes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 194

6.8 Pushouts . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 195

6.9 Truncations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 198

6.10 Quotients . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 201

6.11 Algebra . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 206

6.12 The flattening lemma . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 211

6.13 The general syntax of higher inductive definitions . . . . . . . . . . . . . . . . . . . 216

Notes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 218

Exercises . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 219

7 Homotopy n-types 221

7.1 Definition of n-types . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 221

7.2 Uniqueness of identity proofs and Hedberg’s theorem . . . . . . . . . . . . . . . . . 225

7.3 Truncations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 228

7.4 Colimits of n-types . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 234

7.5 Connectedness . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 238

7.6 Orthogonal factorization . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 243

7.7 Modalities . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 248

Notes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 252

Exercises . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 253

II Mathematics 257

8 Homotopy theory 259

8.1 π1(S1) . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 263

8.2 Connectedness of suspensions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 271

8.3 πk≤n of an n-connected space and πk<n(Sn) . . . . . . . . . . . . . . . . . . . . . . . 272

8.4 Fiber sequences and the long exact sequence . . . . . . . . . . . . . . . . . . . . . . 273

8.5 The Hopf fibration . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 277

8.6 The Freudenthal suspension theorem . . . . . . . . . . . . . . . . . . . . . . . . . . . 283

8.7 The van Kampen theorem . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 289

8.8 Whitehead’s theorem and Whitehead’s principle . . . . . . . . . . . . . . . . . . . . 298

8.9 A general statement of the encode-decode method . . . . . . . . . . . . . . . . . . . 302

8.10 Additional Results . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 303

Notes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 304

Exercises . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 306

9.1 Categories and precategories . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 308

9.2 Functors and transformations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 311

9.3 Adjunctions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 315

9.4 Equivalences . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 316

9.5 The Yoneda lemma . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 322

9.6 Strict categories . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 325

9.7 †-categories . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 326

9.8 The structure identity principle . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 327

9.9 The Rezk completion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 330

Notes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 337

Exercises . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 338

10 Set theory 341

10.1 The category of sets . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 341

10.2 Cardinal numbers . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 350

10.3 Ordinal numbers . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 353

10.4 Classical well-orderings . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 360

10.5 The cumulative hierarchy . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 362

Notes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 368

Exercises . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 368

11 Real numbers 373

11.1 The field of rational numbers . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 374

11.2 Dedekind reals . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 374

11.3 Cauchy reals . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 381

11.4 Comparison of Cauchy and Dedekind reals . . . . . . . . . . . . . . . . . . . . . . . 400

11.5 Compactness of the interval . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 401

11.6 The surreal numbers . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 407

Notes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 419

Exercises . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 420

Appendix 423

A Formal type theory 425

A.1 The first presentation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 427

A.2 The second presentation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 431

A.3 Homotopy type theory . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 438

A.4 Basic metatheory . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 439

Contents ix

Notes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 441

Bibliography 442

Index of symbols 451

Index 457